Inference at * 1 
Iof proof for Lemma p-fun-exp-add-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. n : 
5. can-apply(f^0;x)
  (f^n+0(x)) ~ (f^n(do-apply(f^0;x))) 

latex

 by (((RepUR ``p-fun-exp do-apply`` ( 0)) 
CollapseTHEN (Fold `p-fun-exp` 0)) 
CollapseTHEN (
CRepUR ``p-id`` ( 0))) 
CollapseTHEN (((UnivCD) 
CollapseTHENA (Auto)) 
CollapseTHEN ((
CProveSqEq) 
CollapseTHEN (Auto))) 

latex

C.

Definitions

f^n, do-apply(f;x), p-id(), , {x:A| B(x)} , , A  B, A, False, P  Q, s ~ t, n+m